es:ES, P:(E), d:(e, e':E. Dec(es-p-immediate-pred(es;e.P(e))(e,e'))).
(e:E. Dec(P(e)))
 SWellFounded(p-graph(E;es-r-pred{i:l}(es;d;es-p-immediate-pred(es;e.P(e))))(y,x)) 

latex

Definitions	t  T, {x:A| B(x)} , x:AB(x), , x:A. B(x), E, P  Q, x(s1,s2), es-p-immediate-pred(es;P), x.A(x), x(s), x,y. t(x;y), (e < e'), ES, Dec(P), P & Q, f(a), p-graph(A;f), R1 => R2, x f y, Type, b, can-apply(f;x), es-r-pred{i:l}(es;d;R), suptype(S; T), left + right, s = t, do-apply(f;x), S  T, Top, x:A.B(x), Void, A c B, x:A  B(x), SWellFounded(R(x;y)), t.1, let x,y = A in B(x;y), SQType(T), {T}, s ~ t
Lemmas	es-causl wf, es-r-pred-property, es-causl-swellfnd, do-apply wf, top wf, es-r-pred wf, can-apply wf, assert wf, strongwf-monotone